The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 124 ms)
    ↳4 CdtProblem
    ↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 15 ms)
    ↳6 CdtProblem
    ↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 4 ms)
    ↳8 CdtProblem
    ↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 4 ms)
    ↳14 CdtProblem
    ↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 7 ms)
    ↳16 CdtProblem
    ↳17 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 1 ms)
    ↳22 CdtProblem
    ↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
    ↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
    ↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳30 CdtProblem
    ↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳32 CdtProblem
    ↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳34 CdtProblem
    ↳35 CdtMatrixRedPairProof (UPPER BOUND (ADD(O(n^2))), 16.0 s)
    ↳36 CdtProblem
↳37 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳38 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(.(z0, nil)) → c4(G(z0))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [4] + x1 + x2   
POL(F(x1)) = 0   
POL(G(x1)) = [4]x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(nil) = 0   

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

G(.(z0, nil)) → c4(G(z0))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(nil, z0)) → c1(F(z0))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = x1 + x2   
POL(F(x1)) = [4]x1   
POL(G(x1)) = 0   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(nil) = [4]   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

G(.(z0, nil)) → c4(G(z0))
F(.(nil, z0)) → c1(F(z0))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(7) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, z0)) → c1(F(z0)) by

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
S tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

G(.(z0, nil)) → c4(G(z0))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) by

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
S tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
K tuples:

G(.(z0, nil)) → c4(G(z0))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, nil)) → c4(G(z0)) by

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
S tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
K tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) by

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) by

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) by

F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) by

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
S tuples:

F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) by

F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
S tuples:

F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) by

F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) by

G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) by

G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) by

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
S tuples:

G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) by

G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
S tuples:

G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) by

G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(35) CdtMatrixRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]:
Non-tuple symbols:
M( f(x1) ) =
/0\
\0/
+
/00\
\00/
·x1

M( g(x1) ) =
/0\
\0/
+
/00\
\00/
·x1

M( .(x1, x2) ) =
/0\
\2/
+
/04\
\01/
·x1+
/10\
\01/
·x2

M( nil ) =
/0\
\2/

Tuple symbols:
M( c5(x1) ) =
/0\
\0/
+
/12\
\00/
·x1

M( f(x1) ) =
/0\
\0/
+
/00\
\00/
·x1

M( c1(x1) ) =
/0\
\0/
+
/12\
\01/
·x1

M( c2(x1) ) =
/0\
\2/
+
/10\
\00/
·x1

M( c4(x1) ) =
/0\
\0/
+
/12\
\01/
·x1

M( g(x1) ) =
/0\
\0/
+
/00\
\00/
·x1

M( G(x1) ) =
/0\
\0/
+
/00\
\00/
·x1

M( F(x1) ) =
/0\
\2/
+
/10\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(37) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
nil0() → 0
.0(0, 0) → 0
f0(0) → 1
g0(0) → 2
nil1() → 1
nil1() → 3
f1(0) → 4
.1(3, 4) → 1
.1(0, 0) → 6
.1(0, 6) → 5
f1(5) → 1
nil1() → 2
g1(0) → 7
nil1() → 8
.1(7, 8) → 2
.1(0, 0) → 10
.1(10, 0) → 9
g1(9) → 2
nil1() → 4
.1(3, 4) → 4
f1(6) → 4
f1(5) → 4
.1(0, 6) → 6
nil1() → 7
.1(7, 8) → 7
g1(10) → 7
g1(9) → 7
.1(10, 0) → 10

(38) BOUNDS(O(1), O(n^1))